nLab definable set

Redirected from "type-definable set".
Contents

Contents

Idea

A definable set of an \mathcal{L}-theory TT in a first-order language is an equivalence class of formulas which evaluate the same way in every model of TT. (In the case that TT is empty, Mod(T)\mathbf{Mod}(T) is just the class of \mathcal{L}-structures.)

Definition

Let LL be a first-order language and TT a theory in LL. Any formula ϕ(x 1,,x n)\phi(x_1,\ldots,x_n), whose only free variables could be among x 1,,x nx_1,\ldots,x_n, together with a model MM for TT evaluates to a truth value on each a=(a 1,,a n)M na = (a_1,\ldots,a_n)\in M^n, hence it determines the subset ϕ(M)M n\phi(M)\subset M^n of all aa such that ϕ(a)\phi(a). Two formulas ϕ,ψ\phi,\psi with the same number of free variables are equivalent if ϕ(M)=ψ(M)\phi(M) = \psi(M) for every model MM of TT. A definable set XX in TT is an equivalence class of formulas in LL under this relation. Consider the category el(L)\mathcal{M}_{el}(L) of LL-structures and elementary embeddings and its full subcategory el(T)\mathcal{M}_{el}(T) whose objects are the models of TT. We can also view a definable set for a theory TT as a functor el(T)Set\mathcal{M}_{el}(T)\to Set which is of the form Mϕ(M)M\mapsto\phi(M) for some LL-formula ϕ\phi.

By X(M)X(M) denote the set of all aMa\in M such that X(a)X(a) holds, i.e. ϕ(a)\phi(a) is true for any choice of representative ϕX\phi\in X.

Given two definable sets X,YX,Y in TT a definable function f:XYf: X\to Y is a definable subset of the product sort X×YX\times Y such that f MX(M)×Y(M)f_M\in X(M)\times Y(M) is a function (we also write f M:X(M)Y(M)f_M : X(M)\to Y(M)) for every model MM of TT. Analogously a definable equivalence relation is a definable subset RX×XR\subset X\times X such that R(M)R(M) is an equivalence relation for every model MM of TT.

Properties

Proposition. Given a small category \mathcal{M} and two functors F,G:SetF,G:\mathcal{M}\to Set the natural transformations α:FG\alpha : F\to G are in 1-1 correspondence with functors α˜:Set\tilde\alpha : \mathcal{M}\to Set such that α˜(A)F(A)×G(A)\tilde\alpha(A) \subset F(A)\times G(A) and such that α˜(A)\tilde\alpha(A) is a functional relation.

Proof. If α:FG\alpha:F\to G is an Ob()Ob(\mathcal{M})-indexed family with components α A:F(A)G(A)\alpha_A: F(A)\to G(A) viewed as functional relations α˜ AF(A)×G(A)\tilde\alpha_A\subset F(A)\times G(A), then the extension to a functor means
that there is a (automatically unique) dotted arrow α˜ f\tilde\alpha_f

α˜ A α˜ f α˜ B F(A)×G(A) F(f)×G(f) F(B)×G(B)\array{ \tilde\alpha_A & \stackrel{\tilde\alpha_f}\hookrightarrow & \tilde\alpha_B\\ \downarrow && \downarrow \\ F(A)\times G(A)&\stackrel{F(f)\times G(f)}\longrightarrow & F(B)\times G(B) }

making the diagram commutative (once the existence of α˜ f\tilde\alpha_f is known, the functoriality of α˜ fg=α˜ fα˜ g\tilde\alpha_{f\circ g} = \tilde\alpha_f\circ\tilde\alpha_g comes by uniqueness of α˜ f\tilde\alpha_f and the functoriality of F×GF\times G which it restricts from). That means that for every xF(A)x\in F(A) (x,α A(x))(x,\alpha_A(x)) should be sent to (F(f)(x),G(f)(α A(x)))(F(f)(x), G(f)(\alpha_A(x))) by α˜ f\tilde\alpha_f, what is a restriction of F(f)×G(f)F(f)\times G(f), but by α B\alpha_B being functional relation this must be the same as (F(f)(x),α B(F(f)(x)))(F(f)(x), \alpha_B(F(f)(x))), i.e. that G(f)(α A(x))=α B(F(f)(x))G(f)(\alpha_A(x))=\alpha_B(F(f)(x)). Q.E.D.

In other words, functoriality of α˜\tilde\alpha is the same as α\alpha being natural.

Corollary. Definable functions for LL (for TT) are in 1-1 correspondence with natural transformations of definable sets as functors el(L)Set\mathcal{M}_{el}(L)\to Set (resp. el(T)Set\mathcal{M}_{el}(T)\to Set).

For a fixed (multi-sorted, first-order) theory TT, definable sets and definable functions form a category Def(T)Def(T). This category (or any equivalent category) is the syntactic category of the theory. Models of TT can be recovered as left exact functors Def(T)SetDef(T)\to Set. Notice that definable sets are functors from models to sets, and models are functors from definable sets to sets; just the latter are the “evaluation functionals” among all functors.

See also definable groupoid.

An \infty-definable set is an intersection of definable sets.

We can also consider a relative version of a definable set (definability with parameters).

Given definable sets X,YX,Y, a fixed model MM and a fixed set AX(M)A\subset X(M), we say that an element bY(M)b\in Y(M) is definable over AA if there is (a 1,,a n)A n(a_1,\ldots,a_n)\in A^n and a TT-definable function f:X nYf:X^n\to Y such that f(a 1,,a n)=bf(a_1,\ldots,a_n)=b. All elements bb definable over AA form the subset Y(A)Y(M)Y(A)\subset Y(M). A subset BMB\subset M is definably closed if it is closed under definable functions. Given AMA\subset M, there is the minimal definably closed subset BB such that ABMA\subset B\subset M, the definable closure B=dcl(A)B = dcl(A) of AA.

If we extend the language by the constants from AA we get a new language L AL_A. The definable sets in language LL over AA are the definable sets in language L AL_A over \emptyset.

Ind- and pro-definable sets

One can also study ind-objects and pro-objects in the category of definable sets and definable functions.

Definition

An important special case of a pro-definable set that shows up in model theory are type-definable sets, which are just infinite conjunctions of definable sets. (There is no restriction that the formulas representing these definable sets all sit inside a finite product of sorts.)

References

  • Moshe Kamensky, Ind- and Pro- definable sets, math.LO/0608163

  • Jan Holly, Definable operations on sets and elimination of imaginaries, Proc. Amer. Math. Soc. 117 (1993), no. 4, 1149–1157, MR93e:03052, doi, pdf

  • David Kazhdan, Lecture notes in model theory, pdf

  • D. Haskell, E. Hrushovski, H.D.Macpherson, Definable sets in algebraically closed valued fields: elimination of imaginaries, J. reine und angewandte Mathematik 597 (2006), MR2007i:03040, doi/CRELLE.2006.066)

Last revised on June 23, 2020 at 16:29:28. See the history of this page for a list of all contributions to it.